Deadlock-freeness

Given a system in Orc, the following assertion asks whether the System is deadlock-free or not.

#assert System deadlockfree;

Reachability

Given a system in Orc, the following assertion asks whether P() can reach a state at which some given condition is satisfied.

#assert P() reaches cond;

Consider the metronome example as described in section 3.8.1.1 with GUpdate and #define section added

• globalvar tickNum = 0
• metronome(1000) >> $GUpdate({tickNum = tickNum + 1})>> "tick"
• | Rtimer(500) >> metronome(1000) >> $GUpdate({tickNum = tickNum - 1}) >> "tock"
• #define consecutiveTickOrTock (tickNum < 0 || tickNum > 1)

The #define section defines a condition named as consecutiveTickOrTock which represents the condition such that tickNum is either smaller than 0 or larger than 1. The following assertion queries that whether the System is possible to reach the condition consecutiveTickOrTock.

#assert System reaches consecutiveTickOrTock;

Linear Temporal Logic

In PAT, we support the full set of LTL syntax. Given a system in Orc, the following assertion asks whether the system satisfied LTL property F

#assert System |= F;

where F is an LTL formula whose syntax is defined as the following rules,

F = "p" | prop | [] F | <> F | X F | F1 U F2 | F1 R F2

where p is a publish value, prop is a pre-defined proposition, [] reads as "always" (also can be written as 'G' in PAT), <> reads as "eventually" (also can be written as 'F' in PAT), X reads as "next", U reads as "until" and R reads as "Release" (also can be written as 'V' in PAT).   Consider the metronome example (Section 3.8.1.1), we can query whether the system is always not possible to reach a state that satisfies consecutiveTickOrTock with the following assertion

#assert System |= []!consecutiveTickOrTock ;

we can also query whether the system can always eventually publish value "tick" in the future with the following assertion

#assert System |= []<>"tick";

Reasoning on Non-Reponsive Sites

A non-responsive service is normally up to the operating system to decide when to end the connection. The undeterministic waiting time is not always desirable especially in time-critical system. In time-critical system, the system might expect the value to be received within certain time units, or otherwise, some alternative remedy actions will be done. In such case, proper timeout mechanism need to be introduced to end the non-responsive service if it takes longer than the t time units. Orc has provided such timeout mechanism. As an example, the Orc expression x < x < (Google("Orc") | Rtimer(5) >> ...) will end the Google service if it does not return within 5 time units, where ... denotes the necessary remedy actions. Nonetheless, it is possible that some external services in the system are leaved unhandled for their potential non-responsive behaviour due to human errors. We provide two kinds of assertions for the user to find out unhandled non-responsive site call in their system. The assumption for the checking is that, there is no external parties like operating system that will help to end the non-resposive site call. A special site NRS is used to internally simulate the behaviour of non-reponsive site.

Non-Responsive Site Deadlock (NRSDeadlock)

This is to check whether the non-responsive site call can cause the system deadlock. The following assertion asks whether the system is free of NRSDeadlock behaviour,

#assert System nrsdeadlockfree;

Non-Responsive Site Cycle (NRSCycle)

This is to check whether there exists non-responsive site call that does not cause the system deadlock, but it is always unhandled. Consider expression (S1 >> S2) | S3, if S1 is non-responsive external site call and S3 is always executable (i.e., deadlock-free), the system will still be running smoothly, since S1 and S3 is run on different threads or processors. Nonetheless, S2 will never be run.  The following assertion asks whether the system is free of NRSCycle behaviour,

#assert System nrscyclefree;